T Kurahashi, A. Visser; "Pour-El's Landscape"
メモ
著者による解説
50年代～70年代にかけて行われていた，理論の不完全性，決定不能性，分離不能性に関する研究の中で，特に Pour-El (1968) の結果に注目した研究です．
Tarski-Mostowski-Robinson算術$ \sf Rは本質的不完全，すなわち，$ \sf Rを含む任意の無矛盾な r.e. 理論が不完全，という（Gödel--Rosserの）第1不完全性定理ですが，これは R の本質的決定不能性，すなわち，R を含む任意の無矛盾な理論が決定不能であるという主張と等しいです． Rは更に強い性質を持つことが知られています：
1. 一様本質的不完全性：$ \sf Rの無矛盾な r.e. 拡大理論の r.e. 列 ($ T_i) に対して，全ての $ T_iで独立な文が存在 2. 理論の再帰的分離不能性：$ \sf Rの定理全体の集合$ \mathsf{R}_pと反証可能な文全体の集合$ \mathsf{R}_rついて，$ (\mathsf{R}_p, \mathsf{R}_r)は再帰的分離不能 一様本質的不完全$ \implies本質的不完全
再帰的分離不能$ \implies 本質的決定不能
ですが，実は$ Tが無矛盾な r.e. 理論なら「$ Tは一様本質的決定不能$ \iff再帰的分離不能」となることが Ehrenfeucht (1961) によって示されています．
他方，「本質的決定不能⇒再帰的分離不能」は一般には成立しません．ただ，それぞれの実効版を考えればこの含意が成立する，というのがPour-Elの定理（1968）です． 例えば
$ Tが実効的本質的不完全とは，再帰的関数$ f(x)があって，インデックス$ iをもつ r.e. 集合$ UがT の無矛盾な拡大理論なら，$ f(i)が$ Uから独立な文となることをいいます．第1不完全性定理の証明を考えれば$ \sf Rは実効的本質的不完全です．
決定不能性の実効版は創造性です：
r.e. 理論 T が創造的とは，再帰的関数 $ f(x)が存在して，インデックス$ iをもつ r.e. 集合 $ Xが $ T_pとdisjointなら，$ f(i)が$ X \cup T_pに入らないことを言います．
無矛盾な r.e. 理論について
実効的本質的不完全$ \iff本質的創造的$ \iff実効的分離不能
$ \sf Rは本質的決定不能性より強い性質を持つことが Cobham および Vaught (1962) によって得られています．
すなわち
強再帰的分離不能性：述語論理の定理全体の集合$ 0_pについて $ (0_p, \mathsf{R}_r) は再帰的分離不能 更にこれらの実効版が$ \sf Rに対して成立します．すなわち$ \sf Rは
(I) 実効的本質的創造的
(II) 実効的分離不能
I, IIをそれぞれ強めた概念で，Pour-El の定理より (I)(II) は同値です．
こうした背景から (i)(ii) の同値性が予想されます．
実際，今回の論文の主定理は次のものです：
$ Tを無矛盾な r.e. 理論とすると，以下は同値：
(i) T は実効的本質的遺伝的創造的
(ii) T は強実効的分離不能
他にも不完全性，決定不能性，分離不能性に関わる性質を調べているので，このあたりの話題に興味のある方は是非ご一読いただければと思います．